% !Mode:: "TeX:UTF-8"


\head{Множества}
Множество -- это контейнер элементов одного типа, который обладает свойствами уникальности и неупорядоченности его элементов. Множества бывают конечными и бесконечными.

Типовое выражение для конечного множества: $typeexpr\Set$. Типовое выражение для бесконечного множества: $typeexpr\Infset$. Конечное множество -- подтип бесконечного множества.

Операции над множествами:
\begin{list}{}{}
\item $= : T\Infset \DP T\Infset \Fn \Bool$ -- сравнение на равенство
\item $\neq : T\Infset \DP T\Infset \Fn \Bool$ -- сравнение на не равенство
\item $\Union: T\Infset \DP T\Infset \Fn T\Infset$ -- объединение пары множеств
\item $\Union: T\Infset\Infset \Fn T\Infset$ -- объединение множества множеств
\item $\Inter: T\Infset \DP T\Infset \Fn T\Infset$ -- пересечение пары множеств
\item $\Inter: T\Infset\Infset \Fn T\Infset$ -- пересечение множества множеств
\item $\Minus: T\Infset \DP T\Infset \Fn T\Infset$ -- вычитание множеств
\item $\Isin: T \DP T\Infset \Fn \Bool$ -- проверка на принадлежность
\item $\NotIsin: T \DP T\Infset \Fn \Bool$ -- проверка на непринадлежность
\item $\SetL: T\Infset \DP T\Infset \Fn \Bool$ -- проверка вложения
\item $\SetG: T\Infset \DP T\Infset \Fn \Bool$ -- проверка вложения
\item $\SetLE: T\Infset \DP T\Infset \Fn \Bool$ -- проверка вложения
\item $\SetGE: T\Infset \DP T\Infset \Fn \Bool$ -- проверка вложения
\item $\Card: T\Infset \NonDetermFn \Nat$ -- количество элементов
($\Chaos$ для бесконечных множеств)
\end{list}

Обратите внимание на отсутствие операции выбора произвольного элемента из множества!

Только операция \textbf{card} дает целое число от множеств, т.е. любое целочисленное выражение над множествами будет мощностью некоторого множества.

Конструкторы множеств:
\begin{list}{}{}
\item (\emph{пустое множество}) \{\}
\item (\emph{перечисление}) \{0, 1, 2\} - множество, состоящее из трех целых чисел (не
натуральных!) - нуля, единицы и двойки.
\item (\emph{диапазон}) \{0..2\} -  то же, что и \{0, 1, 2\};
\{0..0\} $\Iden$ \{0\}, \{1..0\} $\Iden$ \{\}
\item (\emph{<<сокращенная запись>>}) $\{ expr\_with\_var | var : typeexpr
\SuchAs boolexpr\}$ (например, $\{2 \star n | n : \Nat \SuchAs n < 3
\}$, что эквивалентно \{0, 2, 4\})
\end{list}

\head{Списки}
Список -- это контейнер элементов одного типа, который обладает свойствами упорядоченности элементов. Для задания списка надо указать не только сами элементы, но и их порядок. Списки бывают конечными и бесконечными.

Типовое выражение для конечного списка: $typeexpr\List$. Типовое выражение для бесконечного списка: $typeexpr\Inflist$. Конечный список -- подтип бесконечного списка.

Операции:
\begin{list}{}{}
\item $=: T\Inflist \DP T\Inflist \Fn \Bool$ -- проверка на равенство
\item $\neq: T\Inflist \DP T\Inflist \Fn \Bool$ -- проверка на не равенство
\item $(.) : T\Inflist \DP \Int \NonDetermFn T$ -- взятие элемента по
индексу ($\Chaos$ для индекса, отсутствующего в списке, индексы
нумеруются \textbf{с единицы})
\item $\Concat: T\List \DP T\Inflist \Fn T\Inflist$ -- конкатенация списков
\item $\Hd: T\Inflist \NonDetermFn T$ -- головной элемент списка ($\Chaos$ для пустого списка)
\item $\Tl: T\Inflist \NonDetermFn T\Inflist$ -- хвостовая часть списка ($\Chaos$ для пустого списка)
\item $\Len: T\Inflist \NonDetermFn \Nat$ -- количество элементов списка ($\Chaos$ для бесконечного списка)
\item $\Elems: T\Inflist \Fn T\Infset$ -- множество элементов списка (без повторений!)
\item $\Inds: T\Inflist \Fn \Nat\Infset$ -- множество индексов элементов списка
\end{list}

Конструкторы списков:
\begin{list}{}{}
\item (\emph{пустой список}) $\LL\LR$
\item (\emph{перечисление}) $\LL 0, 1, 2 \LR$ - список, состоящий из трех целых чисел (не натуральных!) - нуля, единицы и двойки - в порядке увеличения.
\item (\emph{диапазон}) $\LL 0..2 \LR$ -  то же, что и $\LL 0, 1, 2 \LR$; $\LL 0..0 \LR \Iden \LL 0 \LR$, $\LL 1..0 \LR \Iden \LL\LR$
\item (\emph{<<сокращенная запись>>}) $\LL expr\_with\_var | var \In listexpr \SuchAs boolexpr\LR$ (например, $\LL 2 \star n | n \In \LL 0..2 \LR \LR$, что эквивалентно $\LL 0, 2, 4 \LR$)
\end{list}


\head{Отображения}
Отображение -- это множество пар элементов, у которого первые компоненты не повторяются. Отображения бывают конечными и бесконечными, детерминированными и недетерминированными (это те, в которых первые компоненты всё же могут повторяться в разных парах).

Типовое выражение для детерминированного отображения: $$typeexpr_1 \Map typeexpr_2$$ Типовое выражение для недетерминированного отображения: $$typeexpr_1 \NonDeterMap typeexpr_2$$

Операции:
\begin{list}{}{}
\item $=: (T_1 \Map T_2) \DP (T_1 \Map T_2) \Fn \Bool$ -- сравнение отображений на равенство
\item $\neq: (T_1 \Map T_2) \DP (T_1 \Map T_2) \Fn \Bool$ -- сравнение отображений на не равенство
\item $(.): (T_1 \Map T_2) \DP T_1 \NonDetermFn T_2$ -- взятие значения по индексу ($\Chaos$, если значение по этому индексу не
определено)
\item $\Dom: (T_1 \Map T_2) \Fn T_1\Infset$ -- \emph{область определения} отображения
\item $\Rng: (T_1 \Map T_2) \Fn T_2\Infset$ -- \emph{область значения} отображения
\item $\Upd: (T_1 \Map T_2) \DP (T_1 \Map T_2) \Fn (T_1 \Map T_2)$ -- обновление отображения
\item $\Union: (T_1 \Map T_2) \DP (T_1 \Map T_2) \Fn (T_1 \NonDeterMap T_2)$ -- объединение отображений
\item $\Minus: (T_1 \Map T_2) \DP T_1\Infset \Fn (T_1 \Map T_2)$ -- уменьшение отображения
\item $/: (T_1 \Map T_2) \DP T_1\Infset \Fn (T_1 \Map T_2)$ -- проекция отображения
\item $\Superp: (T_2 \Map T_3) \DP (T_1 \Map T_2) \Fn (T_1 \Map T_2)$ -- композиция отображений
\end{list}

Конструкторы отображений:
\begin{list}{}{}
\item (\emph{пустое отображение}) []
\item (\emph{перечисление}) $[0 \mapsto 1, 1 \mapsto 2]$ -- отображение, состоящий из двух пар целых чисел (не натуральных!) - из 0 в 1 и из 1 в 2.
\item (\emph{<<сокращенная запись>>}) $[expr_1\_with\_var \mapsto expr_2\_with\_var | var : typeexpr \SuchAs boolexpr]$ (например, $[n \mapsto n+1 | n : \Nat \SuchAs n < 3]$, что эквивалентно $[0 \mapsto 1, 1 \mapsto 2, 2 \mapsto 3]$)
\end{list}


\subsection*{Задачи}

\zhead{Вычислить выражения с множествами}

\z $\{1, 2\} = \{3, 1\}$
\z $\{1, 2\} = \{2, 1\}$
\z $\{1, 2, 1\} = \{2, 2, 1\}$
\z $\{1, 2\}~\Union~\{3, 4\}$
\z $\{1, 2\}~\Union~\{2, 3\}$
\z $\{1, 2\}~\Inter~\{3, 4\}$
\z $\{1, 2\}~\Inter~\{2, 3\}$
\z $\{1..30\}~\Union~\{10..-10\}$
\z $\{1..30\}~\Inter~\{10..-10\}$
\z $\{1..30\}~\Union~\{x~|~ x: \Int~\SuchAs~\Abs x < 11 \}$
\z $\{1..30\}~\Inter~\{x~|~ x: \Int~\SuchAs~\Abs x < 11 \}$
\z $\{x+10 ~|~ x: \Int \} = \{x ~|~ x: \Int\}$
\z $\{5*k + 2 ~|~ k : \Int \}~\Inter~\{3*k - 1 ~|~ k : \Int\}$
\z $\{5*k + 2 ~|~ k : \Int \}~\Minus~\{3*k - 1 ~|~ k : \Int\}$
\z $\{5*k + 2 ~|~ k : \Int \} \SetL \{3*k - 1 ~|~ k : \Int\}$
\z $\{5*k + 2 ~|~ k : \Int \} \SetGE \{3*k - 1 ~|~ k : \Int\}$
\z $\Not (\{1, 2\} \SetLE \{2, 1, 1\})$
\z $\Card \{1..30\}$
\z $\Card \{5*k + 2 ~|~ k : \Int~\SuchAs~k * k \Isin \{-10..10\}\}$
\z $\Card \{5*k + 2 ~|~ k : \Int~\SuchAs~k * k \Isin \{10..-10\}\}$
\z $\Card \{k*k - 2 * k ~|~ k : \Int~\SuchAs~k * k \Isin \{-10..10\}\}$
\z $\All x: \Nat ~\SuchAs~ x \Isin \{x ~|~ x : \Int\}$
\z $\All x: \Int ~\SuchAs~ x \Isin \{x ~|~ x : \Nat\}$


\zhead{Решите уравнения}

\z $\{1\} \Union x = \{\}$
\z $\{1\} \Union x = \{1\}$
\z $\{1\} \Union x = \{1, 2\}$
\z $\{1\} \Inter x = \{\}$
\z $\{1\} \Inter x = \{1\}$
\z $\{1\} \Inter x = \{1, 2\}$
\z $\{2, 1\} \Minus x = \{1\}$
\z $\Card~x = 0$
\z $\Card~x = 1$


\zhead{Какие из следующих выражений истинные}
Считайте, что свободные переменные располагаются под квантором
всеобщности

\z $(A \cup B) \setminus C = (A \setminus C) \cup (B \setminus C)$
\z $(A \setminus B) \cap C = (A \cap C) \setminus B$
\z $(A \cup B) \setminus C \Iden (A \setminus C) \cup (B \setminus C)$
\z $A \cup \{\} = A$
\z $\{\} \cup A = A$
\z $(A \cup B) \cap C = (A \cap C) \cup (B \cap C)$
\z $\Card \Nat < \Card \Int$
\z $\Card \Nat = \Card \Int$
\z $\Card \Nat > \Card \Int$
\z $\Card \Nat \Iden \Card \Int$
\z $\Card \{n ~|~ n:\Nat\} \Iden \Card \{n ~|~ n:\Int\}$


\zhead{Записать на RSL следующие множества}

\z Пустое множество;
\z Множество чисел 1, 2, 3 (а также множество чисел от 1 до 3);
\z Множество всех чётных чисел;
\z Множество всех чётных чисел, не превышающих 10 (привести в виде перечисления и нескольких различных сокращённых формах);
\z Множество всех простых натуральных чисел;
\z Множество всех пар взаимнопростых натуральных чисел;
\z Множество всех троек, в каждой из которых есть одинаковые элементы;
\z Множество всех степеней двойки, не превышающих 100 (привести в виде перечисления и нескольких сокращённых формах);
\z Множество всех IP-адресов класса А (B, C, D, E);
\z Множество всех точек плоскости, образующих
    \begin{enumerate}
    \item Прямую -- биссектрису I и III квадрантов;
    \item Правую полуплоскость;
    \item Нижнюю полуплоскость;
    \item Единичную окружность;
    \item Единичный круг;
    \item Единичный квадрат со сторонами, параллельными осям
    координат.
    \end{enumerate}

%\zhead{Построить явную спецификацию на RSL для следующих задач}
%
%В этих задачах, если удаётся, следует привести два варианта решения: с использованием сокращённой записи множества
%и с помощью рекурсии.
%
%\z Дано множество чисел. Вернуть множество квадратов чисел данного множества.
%\z Дано множество чисел. Вернуть множество чисел, представимых суммами каких-либо двух элементов исходного множества.
%\z Дано множество точек, заданных координатами в плоской декартовой системе координат. Получить проекцию этого множества на ось \textsc{Ox}.
%\z Дано множество всех простых чисел. Для данного числа вернуть множество его простых делителей, используя множество всех простых чисел.
%\z Дано множество чисел. Дано число. Существует ли подмножество данного множества чисел, сумма элементов которого, равна данному числу.
%\z Дано множество множеств. Вернуть множество всех элементов внутренних множеств.
%\z \textit{(Задача о рюкзаке)} Дано множество предметов. Каждый предмет имеет массу (массы заданы множеством пар предмет >< масса). Есть $n$ рюкзаков. Каждый рюкзак имеет вместимость $K$ кг. Распределить все предметы по рюкзакам, не превышая вместимости каждого рюкзака.
%\z Рабочая группа компьютеров задаётся IP-адресом (4 целых числа, каждое от 0 до 255) и маской (целое число от 0 до 32). Программа по данному заданию строит множество всех возможных в ней IP-адресов.


\zhead{Вычислить выражения со списками}
\z $\LL 1 \LR = \LL 1, 1 \LR$
\z $\LL 1, 2 \LR = \LL 3, 1\LR$
\z $\LL 1, 2\LR = \LL 2, 1\LR$
\z $\LL 1, 2, 3 \LR (2)$
\z $\LL 1 \LR (0)$
\z $\LL 1 \LR (1)$
\z $\LL 1, 2\LR \Concat \LL 3, 4\LR$
\z $\LL 1, 2\LR \Concat \LL 2, 3\LR$
\z $\LL x+10~|~x~\In~\LL 1, 2 \LR \LR = \LL x~|~x~\In~\LL 1 \LR \LR$
\z $\Hd \LL 1, 2, 3 \LR$
\z $\Tl \LL 1, 2, 3 \LR$
\z $\Len \LL 1, 2, 3 \LR$
\z $\Elems \LL 1, 2, 3 \LR$
\z $\Inds \LL 1, 2, 3 \LR$
\z $\Len \LL 1..30\LR$
\z $\Let~x = \LL 1, 2, 3\LR~\In~\Elems~x~\Inter~\Inds~x~\rslEnd$
\z $\Let~x = \LL 0, 1, 2\LR~\In~\Elems~x~\Inter~\Inds~x~\rslEnd$
\z $\Let~x : \Int\Inflist~\SuchAs~(\All i_1, i_2: \Nat~\SuchAs~\Card \{i_1, i_2\} = \Card \{x(i_1), x(i_2)\})\\\In~x~\rslEnd$
\z $\Let~x : \Int\Inflist~\SuchAs~(\All i_1, i_2: \Nat~\SuchAs~\Card \{i_1, i_2\} = \Card \{x(i_1), x(i_2)\})\\\In~\Elems~x~\Inter~\Inds~x~\rslEnd$
\z $\All x : T\Inflist~\SuchAs~x(0) = \Hd x$
\z $\All x : T\Inflist~\SuchAs~x(0) ~\Iden~ \Hd x$

\zhead{Решите уравнения}
\z $\LL 1 \LR \Concat x  = \LL 1 \LR$
\z $\LL 1 \LR \Concat x  = \LL 1, 2, 3 \LR$
\z $\LL 1 \LR \Concat x  = \LL 3, 2, 1 \LR$
\z $\Tl x = \LL 1 \LR$
\z $\Hd x = 1$
\z $x \Concat \Tl x = x$
\z $\Tl x = \LL \Hd x \LR$
\z $\Elems x = \Inds x$
\z $\Elems~\Tl x = \Elems x$
\z $\Len x = \Card \Elems x$
\z $\Len x = \Card \Inds x$
\z $\Len x \Iden \Card \Inds x$


\zhead{Записать на RSL следующие выражения}

\z Пустой список;
\z Список из чисел 1, 2, 3 (попробуйте привести как можно больше различных решений);
\z Список всех простых натуральных чисел в порядке увеличения их значения;
\z Список всех пар взаимнопростых натуральных чисел в порядке увеличения их суммы;
\z Список номеров групп 5го курса факультета ВМиК МГУ в порядке увеличения номера группы;
\z Количество простых чисел от 1 до 10 (тремя различными способами).

%\zhead{Напишите явные спецификации следующих функций}
%
%\z Определить, является ли бесконечным данный список.
%\z Вычислить длину списка без использования функции $\Len$.
%\z Вычислить сумму элементов списка.
%\z Вычислить произведение элементов списка.
%\z Дан список. Построить список из элементов исходного списка, элементы которого идут в обратном порядке по отношению к исходному списку
%\z Дана строка и символ. Определить, встречается ли символ в данной строке (предложить два различных способа решения).
%\z Дана строка. Определить самый часто встречающийся в ней символ.
%\z Отсортировать данный список вещественных чисел в порядке возрастания.
%\z Построить список всех целых чисел в порядке неубывания модуля.
%\z Определить $\sup$ списка вещественных чисел (в случае конечного списка это будет и максимум).
%\z Выдать число, не встречающееся в данном списке.
%\z Дан список чисел. Построить по нему список квадратов, расположив элементы
%    \begin{enumerate}
%    \item с сохранением порядка исходного списка
%    \item в порядке убывания модуля
%    \item так, чтобы не было трёх подряд чисел, расположенных в  порядке возрастания или убывания.
%    \end{enumerate}
%\z Дано натуральное число. Построить список степеней его простых делителей, в котором на местоположение степени есть её основание (а значение, соответственно, показатель).
%\z Дан список показателей степеней (местоположение -- основание степени). Построить соответствующее натуральное число.
%\z Дан список натуральных чисел, отличных от нуля. Вернуть список, в котором на месте №$i$ находится количество раз, которое $i$ встречается в исходном списке.
%\z Дано множество чисел. Построить из него список, расположив элементы множества
%    \begin{enumerate}
%    \item в порядке убывания
%    \item в порядке убывания модуля
%    \end{enumerate}
%\z Дан список чисел. Построить из него новый список, расположив элементы исходного списка
%    \begin{enumerate}
%    \item в порядке убывания
%    \item в порядке убывания модуля
%    \end{enumerate}
%\z Дан список из чисел. Построить из него множество, использовав все элементы данного списка.
%\z Дан множество пар (ключ, объект) и список ключей. Построить соответствующий ему список объектов. Считайте, что во множество пар ключи не повторяются.
%\z Дан список чисел. Можно ли суммой некоторых его элементов получить
%    \begin{enumerate}
%    \item четное число (для списка из целых чисел)
%    \item простое число (для списка из целых чисел)
%    \item целое число (для списка из вещественных чисел)
%    \end{enumerate}


\zhead{Упростить выражения}
\z $\langle x ~|~ x~\In~\langle \Card \{a..b\} \rangle \rangle$
\z $\langle c ~|~ c~\In~\langle 'a',~'b' \rangle \rangle$
\z $\langle c ~|~ c~\In~\langle '$ " $~' \rangle \rangle$
\z $\langle c ~|~ c~\In~\langle \rangle \rangle$

\newcommand{\Masha}{\mbox{\textrm{<<Маша>>}}}
\newcommand{\Sveta}{\mbox{\textrm{<<Света>>}}}
\newcommand{\Misha}{\mbox{\textrm{<<Миша>>}}}
\newcommand{\Slava}{\mbox{\textrm{<<Слава>>}}}
\newcommand{\Anna}{\mbox{\textrm{<<Аня>>}}}
\newcommand{\Petr}{\mbox{\textrm{<<Петя>>}}}
\newcommand{\Lesha}{\mbox{\textrm{<<Леша>>}}}
\newcommand{\Victor}{\mbox{\textrm{<<Витя>>}}}

\zhead{Вычислить}

\z $\map{n \mapsto 1}{n : \Nat \SuchAs n \Isin \{1..3\} }$
\z $\map{n \mapsto n}{n : \Nat \SuchAs n \Isin \{5..5\} }$
\z $\map{n \mapsto n+1}{n : \Nat \SuchAs n \Isin \{100..90\} }$
\z $\map{n \mapsto m}{n, m : \Nat \SuchAs n \backslash m = 0 \And m > 2}$
\z $\map{n \mapsto m}{n, m : \Nat \SuchAs n \Isin \{1..3\} \And m \Isin \{1..n\}}$
\z $\map{n \mapsto (p, q)}{n, p, q : \Nat \SuchAs n \Isin \{1..100\} \And p + q = n \And p \backslash q = 0}$
\z $[1 \mapsto 2,~2 \mapsto 3,~ 3 \mapsto 1] (3)$
\z $[1 \mapsto 2,~2 \mapsto 3,~ 3 \mapsto 1] (4)$
\z $[ \Masha \mapsto 30, \Sveta \mapsto 15, \Masha \mapsto 30] (\Masha)$
\z $[ \Masha \mapsto 30,  \Sveta \mapsto 15, \Masha \mapsto 10 ] (\Masha)$
\z $[1 \mapsto [1 \mapsto 1,~ 2 \mapsto 2,~ 3 \mapsto 3], 2 \mapsto [1 \mapsto 4,~ 2 \mapsto 5,~ 3 \mapsto 6]~]~ (2)~(1)$
\z $\Dom [3 \mapsto 1, 5 \mapsto 0, 2 \mapsto 88]$
\z $\Rng [3 \mapsto 1, 5 \mapsto 0, 2 \mapsto 88]$
\z $\Dom \map{n \mapsto 2 * n}{n : \Nat}$
\z $\Rng \map{n \mapsto 2 * n}{n : \Nat}$
\z $[1 \mapsto 20, 2 \mapsto 30] \Union [1 \mapsto 30, 2 \mapsto 20]$
\z $[1 \mapsto 20, 2 \mapsto 30] \Upd [1 \mapsto 30, 2 \mapsto 20]$
\z $[ \Misha \mapsto 170, \Slava \mapsto 200, \Victor \mapsto 195 ] ~\backslash \\ \{\Misha, \Petr\}$
\z $[ \Misha \mapsto 170, \Slava \mapsto 200, \Victor \mapsto 195 ] ~/ \\\{\Misha, \Petr\}$
\z Пусть Friend = $[\Misha \mapsto \Anna, \Anna \mapsto \Lesha, \Lesha \mapsto \Misha]$. Найти Friend $\Superp$ Friend. Какой смысл этого значения ?
\z $\Card~\Dom~[1 \mapsto 2, 1 \mapsto 3, 2 \mapsto 3]$
\z $\Dom ([10 \mapsto 100, 20 \mapsto 50] \Upd [20 \mapsto 60, 30 \mapsto 90])$
\z $\Card~\Rng~( [1 \mapsto 2] \Superp [3 \mapsto 2, 4 \mapsto 1] \Superp [1 \mapsto 2, 3 \mapsto 4])$

\zhead{Какие из следующих выражений истинны}

Если выражение ложно, привести контрпример и дополнительные ограничения на входящие переменные, чтобы условие стало верным. Считать, что все переменные стоят под кванторами всеобщности.

\z $\Dom~ (X \Union Y) \Iden \Dom X ~\Union~ \Dom Y$
\z $\Rng~ (X \Union Y) \Iden \Rng X ~\Union~ \Rng Y$
\z $\Dom~ (X \Upd Y) \Iden \Dom X ~\Upd~ \Dom Y$
\z $\Rng~ (X \Upd Y) \Iden \Rng X ~\Upd~ \Rng Y$
\z $X = Y ~\Impl~ \Dom X = \Dom Y$
\z $X \NEq Y ~\Impl~ \Dom X ~\NEq~ \Dom Y$
\z $X \NEq Y ~\Impl~ \Rng X ~\NEq~ \Rng Y$
\z $\Dom (X \backslash Y) ~\Iden~ (\Dom X) \backslash Y$
\z $\Dom (X / Y) ~\Iden~ Y$
\z $\Dom (X \Upd Y) ~\Iden~ \Dom X \Union Y$
\z $(X \Union Y) \Union Z ~\Iden~ X \Union (Y \Union Z)$
\z $(X \Upd Y) \Upd Z ~\Iden~ X \Upd (Y \Upd Z)$
\z $(X \Superp Y) \Superp Z ~\Iden~ X \Superp (Y \Superp Z)$
\z $X \Union Y ~\Iden~ Y \Union X$

\zhead{Записать на RSL следующие константы и определения типов}
\z Записать отображение -- перестановку первых $N$ натуральных чисел. Считать $N$ константой с sort-определением.
\z Записать отображение-<<сдвиг>> : [1 $\mapsto$ 2, 2 $\mapsto$ 3, ..., $N \mapsto$ 1]. Считать $N$ константой с sort-определением.
\z Записать отображение всех полных квадратов в своё основание. [1 $\mapsto$ 1, 4 $\mapsto$ 2, 9 $\mapsto$ 3, ...]
\z Записать отображение из любого натурального числа в его простой делитель.
\z Записать отображение любого натурального числа в большее его простое натуральное число. [1 $\mapsto$ 5, 2 $\mapsto$ 7, 3 $\mapsto$ 5, ...]
\z Записать отображение <<бесконечная перестановка>>.
\z Записать отображение любого натурального числа в своё <<зеркало>> -- число из цифр исходного числа, записанных в обратном порядке. [1 $\mapsto$ 1, ..., 12 $\mapsto$ 21, ..., 832 $\mapsto$ 238, ...]
\z Записать отображение любого текста в его реверсию. $[..., \mbox{\textrm{"стол"}} \mapsto \mbox{\textrm{"лотс"}}, \mbox{\textrm{"книга"}} \mapsto \mbox{\textrm{"агинк"}}, ...]$
\z Не меняя описания предыдущей константы, описать новое отображение любого текста, начинающегося с 'a', в его реверсию.
\z Записать тип <<Англо-русский словарь>> так, как Вы его представляете. Учтите, что слово может иметь несколько переводов.

%\zhead{Запишите спецификацию функций в явном виде}
%\z Подсчитать количество элементов в данном отображении, если оно
%    \begin{enumerate}
%    \item детерминированное
%    \item ${^\star}$ недетерминированное
%    \end{enumerate}
%\z По отображению \{[$a \mapsto b$]\} построить отображение \{[$a^2 \mapsto b^2$]\}.
%\z Дано отображение \Nat $\Map$ \Nat. Вернуть количество элементов, отображающих в 0.
%\z По данному отображению \{[$a \mapsto b$]\} построить отображение \{[$b \mapsto x$]\}, где $b$ - правая часть некоторого элемента исходного отображения, а $x$ - количество раз, которое $b$ встретилось в исходном отображении.
%\z Дано отображение \Nat $\Map$ \Nat. Вернуть количество различных элементов, в которые осуществляется отображение.
%\z Дано отображение \Nat $\Map$ \Real, представляющее основание и показатель степени в разложении числа на простые множители. Вернуть число, которое представлено таким отображением.
%\z Дано натуральное число. Построить по нему отображение \Nat $\Map$ \Real, представляющее основание и показатель степени в разложении его на простые сомножители.
%\z Дано отображение строк \{[$s \mapsto t$]\}. Оставить в нём только те элементы, левая часть которого начинается с $s_0$.
%\z Проверить, является ли данное отображение детерминированным.
%\z Проверить, является ли данное отображение конечным.
%\z Проверить, является ли данное отображение взаимнооднозначным.
%\z Проверить, есть ли в данном отображении элемент $x \mapsto y$, где $x$ -- наибольший из всех левых частей, а $y$ -- наименьший среди всех правых частей.
%\z Проверить, является ли данное отображение перестановкой.
%\z Проверить, является ли данное отображение перестановкой первых $N$ натуральных чисел.
%\z Дано отображение \{[$(x, y) \mapsto L$]\} ($L$ -- множество). Проверить, верно ли, что все элементы в $L$ не больше $y$ и не меньше $x$.
%\z Дано отображение. Построить его максимальное детерминированное подотображение.
%\z Реляционное отношение задано отображением $T \Map A \DP B \DP C$. Проверить, есть ли среди атрибутов $A$, $B$, $C$ возможные ключи. Домены атрибутов считать sort-определенными.
%\z Реализуйте функцию $lower$, переводящую символы в нижний регистр. Какова, по Вашему, будет сигнатура этой функции?


\subsection*{Схемы сокращения записи}

Язык RSL обладает достаточно богатыми возможностями для записи выражений. В данном параграфе предлагается освоить ряд приемов по получению более краткой записи выражений за счёт использования различных предопределенных операций над множествами, списками и отображениями.

\paragraph{схема пересечения}

$$x~\Inter~ \{f(t) ~|~ t:T\}$$ вместо $$\{a ~|~ a: X ~\SuchAs~ a \Isin x ~\And~ ( \Exists t: T  ~\SuchAs~ x = f(t) ) \}$$

\paragraph{схема вычитания-1}

$$x ~\Minus~ \{f(t) ~|~ t:T\}$$ вместо $$\{a ~|~ a: X ~\SuchAs~ a \Isin x ~\And~  \Not( \Exists t: T  ~\SuchAs~ x = f(t) ) \}$$

\paragraph{схема вычитания-2}

$$\{f(t) ~|~ t:T\} ~\Minus~ x$$ вместо $$\{a ~|~ a: X ~\SuchAs~ a \NotIsin x ~\And~ ( \Exists t: T  ~\SuchAs~ x = f(t) ) \}$$

\paragraph{схема выборки по ключам (на примере)}
Из исходного отображения выделить подотображение с определенными ключами:
$$t / \{1, 2\}$$ вместо $$[a \mapsto t(a) ~|~ a:X ~\SuchAs~ a \Isin \Dom x ~\And~ a \Isin \{1, 2\} ]$$

\paragraph{схема выборки по значению}
Из исходного отображения выделить подотображение с определенными значениями:
$$[1 \mapsto 1,~ 2 \mapsto 2] \Superp t$$ вместо $$[a \mapsto t(a) ~|~ a:X ~\SuchAs~ a \Isin \Dom x ~\And~ t(a) \Isin \{1,2\} ]$$

%(( all x:X :- ~exists y1, y2: X-set :- y1 ~= y2 /\ x isin y1 inter y2 )) можно записать короче:
%(( ~exists y1, y2: X-set :- y1 ~= y2 /\ y1 inter y2 ~= {} ))
%
%all x:X :- ~exists y:X-set :- x isin y ::::::: ~exists y:X-set :- y ~={} ::::::: all y:X-set :- y = {}

\paragraph{схема соединения (join)}
Для компактной записи выражений, где нужно <<соединение>> двух отображений (join), следует использовать композицию отображений (это ее основное практическое применение).



\subsection*{Задачи}

\zhead{Записать следующие выражения}

При записи решений стараться выбирать наиболее короткую запись.

\z Дано непустое множество натуральных чисел m и натуральное число x. Записать логическое выражение, истинное тогда и только тогда, когда x равен максимальному числу во множестве m.

\textbf{Решение:}

%\begin{lstlisting}
%x isin m /\ (all y: Nat :- y isin m => y <= x)
%\end{lstlisting}
%
%а теперь более короткое решение:

\begin{lstlisting}
x isin m /\ {0..x} >>= m
\end{lstlisting}

\z Дано непустое множество целых чисел m и целое число x. Записать логическое выражение, истинное тогда и только тогда, когда x равен максимальному числу во множестве m.

\z Дано непустое множество натуральных чисел m и натуральное число x. Записать логическое выражение, истинное тогда и только тогда, когда x равен минимальному числу во множестве m.

\z Дано непустое множество натуральных чисел m. Записать сумму элементов этого множества.

\textbf{Решение:}
\begin{lstlisting}
card {(x,y)| x, y : Nat :- x isin m /\ y < x}
\end{lstlisting}

\z Дано непустое множество целых чисел m. Записать сумму элементов этого множества.

\z Дано непустое множество натуральных чисел m. Записать произведение элементов этого множества.

\z Дан непустой список t, натуральное число x и значение y того же типа, каков тип элементов в t. Записать логическое выражение, истинное тогда и только тогда, когда x является индексом первого вхождения y в t.

\z Дан непустой список t, натуральное число x и значение y того же типа, каков тип элементов в t. Записать логическое выражение, истинное тогда и только тогда, когда x является индексом последнего вхождения y в t.

\z Дан непустой список t, натуральные числа x1 и x2 (x2 > x1) и значение y того же типа, каков тип элементов в t. Записать логическое выражение, истинное тогда и только тогда, когда x1 и x2 являются индексами двух подряд вхождений y в t.

\z <<особые фамилии>>. Дано множество <<фамилий>> t. Записать множество фамилий из t, оканчивающихся на <<ов>>.

\textbf{Решение:}
\begin{lstlisting}[escapechar={@}]
t inter {z ^ @"ов"@ | z: Text}
\end{lstlisting}

\z Даны две строки t1 и t2. Записать логическое выражение, истинное тогда и только тогда, когда t2 является подстрокой строки t1.

\z Дана строка t. Записать выражение, равное реверсу строки t.

\z Дано отображение m некоторого типа в тот же тип. Записать логическое выражение, истинное тогда и только тогда, когда это отображение является перестановкой.

\z Дано отображение db строк в целые числа, причем все целые числа разные (например, эти числа - это какие-нибудь хэш-значения строк). В db добавляется строка t и получается db2 (всё остальное соответствие строк и целых чисел из db сохраняется, добавляется новое без нарушения свойства различия целых чисел). Записать логическое выражение, определяющее db2.

\textbf{Решение:}
\begin{lstlisting}[escapechar={@}]
db2 \ {t} = db /\ t isin dom db2 /\ db2(t) ~isin rng db
\end{lstlisting}

Обратите внимание, что сразу два требования (что сохраняются все строки и сохраняется соответствие строк и целых чисел) записано в первом конъюнкте. Обратите также внимание, что хоть и неизвестно целое число, поставленное в соответствие строке t в db2, возможно записать ряд важных свойств отображения db2.

\z Игровое поле игры <<крестики-нолики>> задано следующим способом:
\begin{lstlisting}
type Cell == empty | cross | toe
type Nat3 = {| n: Nat :- n isin {1..3} |}
type Field = (Nat3 >< Nat3) -m-> Cell
\end{lstlisting}
Дано f --- значение в типе Field. Записать
\begin{enumerate}
  \item логическое выражение, истинное тогда и только тогда, когда в отображении f есть информация обо всех клетках поля;
  \item выражение, равное числу пустых клеток.
\end{enumerate}

\z\label{z:correct_graph} Граф задан отображением вершин во множество инцидентных им вершин:
\begin{lstlisting}
type V, G = V -m-> V-set
\end{lstlisting}
Такое представление будет считаться <<корректным>>, если каждая вершина встречается среди первых компонент отображения (при отсутствии инцидентных вершин значение в отображении для такой вершины будет пустым множеством). Записать логическое выражение, истинное тогда и только тогда, когда данная переменная g типа G является <<корректным>> представлением графа.

\z Дано <<корректное>> представление g графа (см. задачу~\ref{z:correct_graph}) и список вершин p. Записать логическое выражение, истинное тогда и только тогда, когда p является путём в графе g.

\z Дано <<корректное>> представление g графа (см. задачу~\ref{z:correct_graph}) и его вершина v. Записать выражение, равное множеству вершин, достижимых из v через не более одну промежуточную вершину.

\textbf{Решение:}

\begin{lstlisting}
g(v) union (g#g)(v)
\end{lstlisting}

чуть более длинный вариант:
\begin{lstlisting}
g(v) union union rng (g/g(v))
\end{lstlisting}

\z Дано <<корректное>> представление g графа (см. задачу~\ref{z:correct_graph}) и его вершина v. Записать выражение, равное множеству вершин, которым инцидентна v.


\z В таксопарке есть следующая база:
\begin{lstlisting}[escapechar={@}]
type @Водитель@, @Машина@, @Водители@ = @Водитель@ -m-> @Машина@
\end{lstlisting}
Дана b --- база водителей с машинами.
\begin{enumerate}
  \item Дана машина c. Найти всех водителей машины c.
  \item Найти множество всех различных машин.
  \item У таксопарка есть доступ к базе машин:
\begin{lstlisting}[escapechar={@}]
type @Машина@, @Цвет@, @Машины@ = @Машина@ -m-> @Цвет@
\end{lstlisting}
Дана m --- база машин с их цветами. Найти водителей, которые ездят на 'красных' машинах.
\end{enumerate}


\zhead{Спецификация алгоритмов со структурами данных\footnote{Алгоритмы взяты из книги~\cite{structures_algorithms}}}

В этих задачах требуется переписать приведенные классические алгоритмы работы со структурами данных на RSL. Следите за тем, чтобы спецификация оставалась <<читабельной>>. Вам пригодится конструкция <<неявный let>>.

\z <<Алгоритм Дейкстры>>. Алгоритм предназначен для решения задачи нахождения кратчайших путей в ориентированном графе с неотрицательными пометками вершин. Длина пути --- это сумма пометок входящих в него дуг. В приведенном псевдокоде ищутся пути от вершины 1, остальные вершины графа пронумерованы числами от 2 до n, V --- это множество чисел от 1 до n. C[i,j] дает пометку дуги из i в j, или $\infty$, если такой дуги нет. Результат помещается в переменную S.

\begin{verbatim}
S := {1};
for i := 2 to n do
  D[i] := C[1,i];
for i := 1 to n-1 do
begin
  выбор из множества V\S такой вершины w,
     что значение D[w] минимально;
  добавить w к S;
  for каждая вершина v из множества V\S do
    D[v] := min(D[v], D[w]+C[w,v])
end
\end{verbatim}

% алгоритм Флойда

\z <<Алгоритм Прима>>. Алгоритм предназначен для решения задачи нахождения остовного дерева минимальной стоимости. Остовное дерево содержит все вершины исходного графа, но возможно не все его дуги. В алгоритме V --- это множество вершин (множество чисел от 1 до n). Результат формируется в дереве T.

\begin{verbatim}
T := пустое дерево;
U := {1};
while U не равно V do
begin
  (u,v) --- ребро наименьшей стоимости такое, что
    u принадлежит U и v принадлежит V\U;
  добавить в T (u,v);
  добавить в U v;
end
\end{verbatim}

% алгоритм Крускала

% алгоритм Прима

% разные остОвные подграфы

% поиск подслов

